\begin{tabbing}
with decls ${\it ds}$ ${\it da}$sends on $l$ from $e$ include $f$($e$) and only these for tags in ${\it tgs}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:E.\+\+
\\[0ex]isrcv($e$)
\\[0ex]$\Rightarrow$ lnk($e$) $=$ $l$
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:E. isrcv(${\it e'}$) \& lnk(${\it e'}$) $=$ $l$ \& (tag(${\it e'}$) $\in$ ${\it tgs}$) \& sender(${\it e'}$) $=$ sender($e$))
\\[0ex]$\Rightarrow$ (tag($e$) $\in$ ${\it tgs}$))
\-\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex]isrcv(${\it e'}$) $\Rightarrow$ lnk(${\it e'}$) $=$ $l$ $\Rightarrow$ (tag(${\it e'}$) $\in$ ${\it tgs}$) $\Rightarrow$ valtype(${\it e'}$) $\subseteq\rho$ ${\it da}$(kind(${\it e'}$))?Void)
\-\\[0ex]\& ($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]\& \=$\forall$$e$@source($l$).\+
\\[0ex]$\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$f$($e$)$\parallel$}}$.
\\[0ex]$\exists$${\it e'}$:E. isrcv(${\it e'}$) \& lnk(${\it e'}$) $=$ $l$ \& (tag(${\it e'}$) $\in$ ${\it tgs}$) \& sender(${\it e'}$) $=$ $e$ \& index(${\it e'}$) $=$ $i$
\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex]isrcv(${\it e'}$)
\\[0ex]$\Rightarrow$ lnk(${\it e'}$) $=$ $l$
\\[0ex]$\Rightarrow$ (tag(${\it e'}$) $\in$ ${\it tgs}$)
\\[0ex]$\Rightarrow$ index(${\it e'}$)$<\parallel$$f$(sender(${\it e'}$))$\parallel$ \& $\langle$tag(${\it e'}$)$,\,$val(${\it e'}$)$\rangle$ $=$ $f$(sender(${\it e'}$))[index(${\it e'}$)])
\-\-\-
\end{tabbing}